docs(errata): PR1 of 2 — false-claim corrections from #4984 campaign errata - #5030

`freeEnergyAlongExhaustion_latticeGraph_eq_log_div_card` was documented as
an "alternate form of `freeEnergyAlongExhaustion_eq_inv_card_mul_log` using
the Fintype-card expression", but the lemma it names already uses
`Fintype.card`, so no distinction is being drawn. The doc now records that
the two conclusions are the same proposition and differ only in the ambient
lemma delegated to, and points at
`freeEnergyAlongExhaustion_latticeGraph_eq_inv_Λcard_mul_log` as the
genuinely different cardinality spelling.

Verified in Lean: `@..._eq_log_div_card = @..._eq_inv_card_mul_log := rfl`
is accepted, at both the lattice-graph and the ambient layer. Comment-only;
no declaration is added, removed or renamed.

Refs #5000

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

`correlationInfinite_le_const_mul_beta_of_high_temp` was documented as
holding "For `0 ≤ J`, `1 ≤ d`, `0 < b` ...", but its binder telescope
carries no `1 ≤ d`; the dimension bound is dropped from the prose.

`freeEnergyComplex_continuousAt_real_pos_h_latticeGraph` was documented as
continuity at "real positive `h₀`", but it takes `(h₀ : ℝ)` with no
positivity hypothesis and holds at every real `h₀`. The headline is
corrected and the mismatch with the `_pos_h_` in the name is recorded.

Both telescopes read off `#check`. Comment-only; the names are left alone,
since renaming is a separate decision.

Refs #5002

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

correlation length

Three sites asserted that `−log tanh(βJ)`, or a finite-region infimum of
per-pair pseudo-masses, *is* the inverse correlation length. The tree
proves only bounds: `latticeMass_le_neg_log_tanh_betaJ`,
`latticeMass_two_sided_bound`, and
`onAxisInverseCorrelationLength_le_neg_log_tanh` are all inequalities, and
no equality with that rate exists anywhere.

* `UnconditionalFiniteRegionLipschitz.lean` header: "faithful
  inverse-correlation-length rate" -> "direct-path rate", the name the
  neighbouring `LatticeMassHighTemperature/UpperBound.lean` already uses.
* `finiteRegionPseudoMassDist`: the claim that the finite infimum "is the
  genuine inverse correlation length restricted to `A`" is replaced by the
  faithful-radius statement plus an explicit note that no relation to
  `latticeMass` is proved here. Measured at the merge base: the file sets
  mentioning `finiteRegionPseudoMassDist` (24) and `latticeMass` (85)
  intersect in zero files.
* `docs/index.md` #4333 row: it simultaneously claimed the `hprofile` of
  #4330-#4332 "is now an unconditional theorem" and, in parentheses, that
  the theorem is at a different rate. The row now states that the
  unconditional bound does not discharge that binder -- `#check` shows the
  binder is `pseudoMassG α ρ (−log(βJ·2d))` at a fixed radius while the
  theorem is `pseudoMassG α (latticeDistance d x z) (−log tanh(βJ))` -- and
  names the rate-agnostic engine as what it does discharge.

Lean changes are comment-only. `citation_audit.py` is unaffected: the
findings/ratchet counts are identical with the merge base's `docs/index.md`.

Refs #5005

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

The docstring of `truncated4Infinite_J_zero_of_pairwise_distinct` called
the closed form `-2·tanh(β·h)^4` "(non-vanishing)". `Ferromagnetic ⟨0,h,β⟩`
only requires `0 ≤ h`, so `h = 0` is admissible and there the form is `0`.

Replaced by the zero/nonzero split over the admissible range, matching the
already-corrected sibling in `TwoPointTruncatedTrivialSlices.lean`. Both
halves checked in Lean: `-2 * Real.tanh (β * 0) ^ 4 = 0`, and
`-2 * Real.tanh (β * h) ^ 4 < 0` for `0 < h`, `0 < β`. The surrounding
`-2·t⁴ ≤ 0` sentence was correct and is kept. Comment-only.

Refs #5008

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

`partitionFunctionAlongExhaustion_high_temp_expansion_h_zero_pow_two_lt_of_nonempty`
was documented as holding "under nonempty volume". Its hypotheses are
`0 < β * J` and `0 < |E|`; it takes no `(Λ.volume n).Nonempty`, unlike the
`_of_nonempty` wrappers in `HighTemperatureBoundsRatioLogFeNonempty`, which
do take it and convert it with `hne.card_pos`.

The doc now names the hypotheses it actually has and records the divergence
from its siblings. Telescope read off `#check`. Comment-only; the duplicate
declaration itself is left in place.

Refs #5011

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

* `magnetizationΛ_ge_tanh`: "`|A|^1 = |A|.card = 1`" is not a well-formed
  identity. Replaced by the wording already used for the parallel
  `magnetizationInfinite_J_zero`: `A.card = 1`, so the power reduces to
  `tanh(β·h)` -- which is exactly what the proof's `Finset.card_singleton`
  rewrite does.
* `correlationAlongExhaustion_J_zero_of_subset` and
  `correlationInfinite_J_zero` called the `J = 0` slice the
  "infinite-temperature slice". Infinite temperature is `β → 0`; `J = 0` is
  the non-interacting slice, and `β` is free in the first while the second
  requires `0 < β` through `Ferromagnetic`. Both now say what
  `MagnetizationInfinite/TrivialSlices.lean` already says.
* `susceptibilityInfinite`: the doc asserted `|χ_Λ(i)| ≤ 2·|Λ|` as an
  available fact. No such bound exists in the tree (that string occurs
  nowhere else). Replaced by the provable point the sentence was making --
  `susceptibility` sums `truncated2` over the volume, so the summand count
  grows with the stage and no stage-uniform bound is proved here.
* `susceptibilityInfinite_le_abs_h`: cited `ciSup_le_ciSup`, which does not
  exist at this mathlib pin. The proof applies `ciSup_mono`.

Comment-only.

Refs #5017

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

* `partitionFunctionΛ_high_temp_expansion_h_zero_closed_evenSubgraphs`
  carried an odd number of `**` markers, so its bold span did not close
  where it appeared to. Stray marker removed.
* Declaration docs across `Analyticity*` use `pFE`, `vdSum` and `ε(t)` as
  if they named definitions. `vdPolymerFamilies_sum` and its `.erase ∅`
  variant have no definition at all -- they are written out in full in
  every statement -- and neither `pFE` nor `vdSum` is introduced anywhere.
  Each affected module header now carries the expansion and says these are
  prose shorthands rather than library names, extending the legend device
  the same headers already use for `Ξ` and `ε`.

`AnalyticityLambdaMayerRecurrenceEpsilon` and
`AnalyticityLambdaMayerPfeEdgeBounds` are unchanged: their headers already
introduce `ε t` as a shorthand with no definition behind it, which is the
only shorthand their declaration docs use.

Comment-only.

Refs #5019

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

`partitionFunctionΛ_high_temp_expansion_h_zero_upper_bound` was documented
as a "ℤ^d wrapper". `#check` shows it is stated for an arbitrary
`G : SimpleGraph V` over an arbitrary `V` with `Λ : Finset V`; nothing in
its signature or proof mentions `latticeGraph`, `cubicExhaustion` or any
other ℤ^d construct. In the `AmbientLattice/` tree ℤ^d vocabulary is what
has to be absent, since the layer is graph-generic and the specializations
live downstream in `Concrete/`.

Reworded to the form its siblings in the same file already use, naming the
wrapped `IsingModel.partitionFunction_high_temp_expansion_h_zero_upper_bound`.
The provenance token in the sentence is re-emitted unchanged. Comment-only.

Refs #5022

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

difference is not a ratio

* `freeEnergyInfinite_high_temp_h_zero_upper_bound_exp_uniform` was
  advertised as "globally tighter than `freeEnergyInfinite_le_uniform_upper_bound`
  at `h = 0` (the cosh-based bound)". Both claims are wrong. The right-hand
  sides are the same real number under this theorem's hypotheses --
  `log 2 + |β|·(|J|·c + |0|) = log 2 + β·J·c` for `0 ≤ J`, `0 < β`, checked
  in Lean -- and the named lemma's conclusion contains no `Real.cosh` at
  all; `cosh` enters only through the lower bound used for coboundedness.
* `freeEnergyInfinite_high_temp_h_zero_ratio_bound` and its `_beta_zero`
  companion are headlined as "ratio upper bound" while their conclusions
  bound a difference, which their own doc bodies display two lines below.
  Both headlines corrected, each noting that the `_ratio_bound` in the name
  does not describe the statement.

Renames are a separate decision and are not made here. Comment-only.

Refs #5026

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…unds do exist

Round-1 review follow-up on this branch's own prose fixes.

docs/index.md, the #4333 row:
* the title asserted it discharges the section 17.5 `hprofile` while the body
  denied it; retitle to the direct-path rate and to the engine's ratio
  hypothesis, matching the body;
* "never by an equality" was false: `latticeMass_one_eq_correlationMass` proves
  `latticeMass 1 (cubicExhaustion 1) = ofReal(correlationMass (beta*J))` with
  `correlationMass a = -log tanh a`. State the true shape: upper bounds only for
  general `d` (`latticeMass_le_neg_log_tanh_betaJ`, bundled in
  `latticeMass_two_sided_bound`, plus the sharper on-axis inequality), equality
  in `d = 1` only;
* the `hprofile` binder is a fixed radius in #4330/#4331 but the pair distance
  in #4332; the rate, not the radius, is what separates them, so replace the
  hedge with the source module's own ruling that this bound is strictly weaker;
* the rate-agnostic engine's `hratio` carries no rate; #4333 discharges the
  profile bound that supplies it.

docs/index.md, the #4334 row: `hprofile` named two different objects in one row;
the second occurrence is now described as the engine's ratio hypothesis.

`MagnetizationInfiniteSusceptibility.lean`: the claim that no stage-uniform
bound exists and that `susceptibility_nonneg` is the only sign/size fact is
refuted by `susceptibilityAlongExhaustion_le_of_high_temp`,
`susceptibilityAlongExhaustion_bddAbove_latticeGraph_of_high_temp` (which
discharges the `BddAbove` hypothesis this same docstring points at) and
`susceptibilityInfinite_J_zero`. Also align "grows" with the module header's
"nondecreasing".

`FiniteRegionPseudoMassDistContinuity.lean`: the global envelope reaches
`latticeMass` from below with no constant
(`globalPseudoMassDist_le_latticeMass`); only the reverse direction carries one.

Terminology: "faithful" named the radius elsewhere in the tree but was also
used for the tanh rate; the rate is now uniformly "direct-path" across
`UnconditionalFiniteRegionLipschitz.lean`, `MassContinuityPairMassUpperIcc.lean`
and their `docs/index.md` rows.

Shorthand legends: cover `vdSum_tanh`, the parenthesised-activity forms and the
section comments that use them, and introduce the forms in the two Mayer
modules that used them without one.

Comment-only in Lean; `lake build` clean.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…ld bound is not an |h| bound

Row 1901 (#4333) in docs/index.md compared the direct-path rate
`-log tanh(betaJ)` with the Simon-Lieb rate `-log(betaJ*2d)` and concluded
"strictly weaker, does not discharge" for all of #4330-#4332. A rate-only
comparison closes only at a common radius, which is #4332's
`latticeDistance d x z`. In #4330/#4331 the radius `rho` is a free variable,
and `pseudoMassG a r t = 2*exp(-(t*r))/(1+(t*r)^a)` sees rate and radius only
through the product `t*r`, so the theorem does supply their binder at every
radius with `rho*(-log(betaJ*2d)) >= dist x z*(-log tanh(betaJ))` -- for
instance at every `rho >= 2*dist x z`, where the criterion reads
`(betaJ*2d)^2 <= tanh(betaJ)` and the window gives it with room to spare.
The row now scopes the strict-weakening to #4332 and states the product
criterion for the free-radius pair; the row title carries the matching
"uniformly in its radius" qualifier. The source module
`UnconditionalProfileLower.lean` already scoped this correctly.

`AmbientLattice/MagnetizationInfiniteSusceptibility.lean` claimed that
`susceptibilityAlongExhaustion_bddAbove_latticeGraph_of_high_temp` discharges
the `BddAbove` hypothesis of `susceptibilityInfinite_le_abs_h`. The provider
concludes `BddAbove` at `<J, 0, beta>` and the consumer asks for it at
`<J, |h|, beta>`, so it applies only at `h = 0`, where that comparison is an
identity. The docstring now states that scope.

Comment-only in Lean; `lake build` clean, `audit_gate.py --full` PASS,
header-claim ratchet 151/79 unchanged.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…he distance

The row's trailing clause "does not imply it at smaller rho" attaches, on its
nearest-antecedent reading, to the example radius 2*dist x z, where it is false:
the rate ratio (-log tanh(beta*J))/(-log(beta*J*2d)) stays below 1.54 on the
window, so every rho in [dist*ratio, 2*dist) already discharges the binder.
Attach the negation to the criterion itself, and state the 2*dist reduction at
the radius where it is an equivalence rather than as the criterion at large.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>